\begin{tabbing}
$\vdash$  \=$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)), $P$:($A$$\rightarrow\mathbb{P}$), $p$:($\forall$$x$:$A$. Dec($P$($x$))).\+
\\[0ex]p{-}co{-}restrict($f$;$p$) $\in$ $A$$\rightarrow$($B$ + Top)
\-
\end{tabbing}